跳转至

文章背景与核心概要

随着大语言模型（LLM）在软件工程领域的深入应用，“验证代码生成（Verified Code Generation）”成为了一个关键前沿方向。该任务不仅要求模型生成可执行程序，还要求生成能够通过机器检查的、证明该程序符合形式化规范的数学证明。然而，传统的开发流程通常采用解耦的顺序管道：先生成程序，再尝试编写证明。这种孤立的做法往往导致代码结构不利于验证，从而陷入脆弱且低效的修复循环中。

为了解决这一痛点，本文作者受计算机科学先驱迪杰斯特拉（Dijkstra）“程序与正确性论证应当携手并进”这一理念的启发，提出了一种基于LLM的智能体工作流——\(\text{P}^3\)。该方法的核心在于从形式化规范中直接推导出一个“统一的程序与证明计划”，并在该共享的架构蓝图下共同细化实现与证明支架。此外，作者还推出了基于真实世界软件仓库构建的基准测试集 Lean4Commit0，用于在更具挑战性的库级别场景下评估验证代码生成的性能。实验结果表明，\(\text{P}^3\) 在多个基准测试中显著提升了求解率，同时大幅降低了API调用成本和计算耗时。

\(\text{P}^3\): Joint Program-and-Proof Planning for Verified Code Generation

arXiv ID: 2608.09277
Primary Subject: Artificial Intelligence (cs.AI)
Secondary Subject: Programming Languages (cs.PL)
Authors: Zenan Li, Ziran Yang, Peiyang Song, Zhaoyu Li, Kaiyu Yang
Submitted On: August 10, 2026

Summary

验证代码生成任务要求大语言模型（LLM）同时生成可执行程序以及机器可检查的证明，以确保程序符合形式化规范。传统上，这一过程被拆分为一个串行管道：先生成程序，然后尝试证明其正确性。

然而，这种解耦的工作流往往被证明是低效且脆弱的。在编写程序时如果没有预先考虑到验证的需求，代码往往会包含细微的错误或不必要的复杂结构，从而极难进行验证，导致繁琐的修复循环。

为了解决这个问题，作者推出了 \(\text{P}^3\)，这是一个基于 LLM 的智能体工作流，灵感来源于迪杰斯特拉的原则，即程序和正确性论证应该同步开发。\(\text{P}^3\) 的工作方式如下： 1. 直接从规范中推导出一个统一的程序与证明计划。 2. 在这个共享的架构计划下，进一步细化实现和证明支架。

此外，为了在真实场景中对验证代码生成进行基准测试，作者提出了 Lean4Commit0，这是一个基于真实世界软件仓库提取的、库级别的基准测试（包含跨 API 的关系规范，并已翻译成 Lean 任务）。

关键结果

  • 更高的求解率： 在四个前沿 LLM 后端的所有测试基准（Verina、AlgoVeri 和 Lean4Commit0）上均优于基线方法，在困难子集上的求解率提升了 4.6 到 11.2 个百分点。
  • 更高的效率： 每个任务的 API 成本降低了高达 ~40%，实际耗时减少了高达 ~37%。
  • 消融实验验证： 相比仅进行实现的规划，性能提升了 3.3 到 8.3 个百分点，证实了联合进行程序与证明规划的独特优势。

Verified code generation tasks Large Language Models (LLMs) with producing both an executable program and a machine-checkable proof that the program adheres to a formal specification. Traditionally, this process is decoupled into a sequential pipeline: generating the program first, and then attempting to prove its correctness.

However, this decoupled workflow often proves inefficient and brittle. Programs written without foresight into their verification requirements frequently contain subtle errors or structures that are needlessly difficult to verify, leading to cumbersome repair loops.

To address this, the authors introduce \(\text{P}^3\), an LLM-based agentic workflow inspired by Dijkstra’s principle that programs and correctness arguments should be developed in tandem. \(\text{P}^3\) operates by: 1. Deriving a unified program-and-proof plan directly from the specification. 2. Elaborating the implementation and proof scaffold under this shared architectural plan.

Additionally, to benchmark verified code generation in realistic scenarios, the authors present Lean4Commit0, a repository-derived, library-level benchmark extracted from real-world software repositories (complete with relational specifications across APIs translated into Lean tasks).

Key Results

  • Higher Solve Rates: Outperforms baseline methods across all tested benchmarks (Verina, AlgoVeri, and Lean4Commit0) using four frontier LLM backends, improving solve rates by 4.6 to 11.2 percentage points on difficult subsets.
  • Increased Efficiency: Reduces per-task API costs by up to ~40% and wall-clock time by up to ~37%.
  • Ablation Validation: Demonstrates a 3.3 to 8.3 point gain over implementation-only planning, confirming the distinct advantage of joint program-and-proof planning.

Abstract

验证代码生成要求大语言模型（LLM）生成可执行程序以及机器可检查的证明，以确保程序满足形式化规范，从而有望实现构建时即正确的软件。事实上的工作流将问题的两半解耦：首先合成程序，然后尝试证明其正确性。我们观察到，这种顺序管道在实践中既无效又低效。在没有预料到证明的情况下生成的程序可能存在隐蔽的错误或在结构上难以验证，迫使 LLM 陷入在修改代码和修改证明之间交替的脆弱修复循环中。受迪杰斯特拉关于程序与其正确性论证应当携手并进的观点的启发，我们提出了 \(P^3\)，这是一个基于 LLM 的智能体工作流，它首先从规范中推导出一个统一的程序与证明计划，然后在此共享计划下细化实现和证明支架。为了在现实环境中评估验证代码生成，我们进一步推出了 Lean4Commit0，这是一个由仓库衍生的、库级别的基准，通过从真实世界软件仓库中提取核心 API，并将其需求（包括跨 API 的关系规范）转化为 Lean 任务构建而成。使用四个前沿 LLM 后端，我们在 Verina、AlgoVeri 以及我们的 Lean4Commit0 基准上评估了 \(P^3\)，它在每个基准-模型设置中都取得了最高的求解率。与更强的基线相比，它在每个基准的困难子集上的求解率提高了 4.6--11.2 个百分点，并将每个任务的 API 成本降低了约 40\%，实际运行时间减少了约 37\%。针对性的消融实验进一步显示，相比仅进行实现的规划，其性能提升了 3.3--8.3 个百分点，从而凸显出联合规划程序与证明的好处。

Verified code generation asks a large language model (LLM) to generate both an executable program and a machine-checkable proof that the program meets a formal specification, promising software that is correct by construction. The de facto workflow decouples the two halves of the problem: first synthesize a program, then attempt to prove it correct. We observe that this sequential pipeline can be both ineffective and inefficient in practice. A program generated without anticipating its proof can be subtly incorrect or structurally difficult to verify, forcing the LLM into brittle repair loops that alternate between patching the code and patching the proof. Inspired by Dijkstra's view that a program and its correctness argument should be developed hand in hand, we propose \(P^3\), an LLM-based agentic workflow that first derives a unified program-and-proof plan from the specification, then elaborates the implementation and proof scaffold under this shared plan. To evaluate verified code generation in realistic settings, we further introduce Lean4Commit0, a repository-derived, library-level benchmark built by extracting core APIs from real-world software repositories and translating their requirements, including relational specifications across APIs, into Lean tasks. Using four frontier LLM backends, we evaluate \(P^3\) on Verina, AlgoVeri, and our Lean4Commit0 benchmark, where it achieves the highest solve rate in every benchmark--model setting. Compared with the stronger baseline, it improves solve rates by 4.6--11.2 percentage points and reduces per-task API cost by up to roughly 40\% and wall-clock time by up to roughly 37\% on the difficult subset of each benchmark. A targeted ablation further shows gains of 3.3--8.3 points over implementation-only planning, isolating the benefit of planning the program and proof jointly.